poss:(ES{i}Prop{i'}), T:Type{i}, s:T, i:Id, P:(possible-event{i:l}(poss)Prop{i'}),
R:(possible-event{i:l}(poss)possible-event{i:l}(poss)Prop{i'}), Rs:(TTProp{i'}).
(Trans _1,_2:T. Rs(_1,_2))
 (es:ES{i}, e:E. poss(es)  state@i  T  loc(e) = i  Rs((state when e),state after e))
 (es:ES{i}.
 (poss(es)  state@i  T  @i stable s.ma-knows{i:l}(poss; i; T; s; P; Rs; R)  ) 

latex

Definitions	t  T, {T}, P  Q, x:A. B(x), SQType(T), Id, s = t, Prop, s ~ t, Atom$n, state@i, (state when e), x:AB(x), ES, f(a), 1of(t), E, x:AB(x), PossibleEvent(poss), pe-es(e), pe-state(p), Type, Trans x,y:T. E(x;y), P & Q, A & B, poss-consistent(i;T;s;ev;R), x,y. t(x;y), loc(e), P  Q, b, P  Q, e@i. P(e), a = b, x.A(x), x. t(x), K(P)@e, @i stable state.P(state)  , Ki(P)@s, state after e, , pe-e(p)
Lemmas	pe-es wf, pe-e wf, all functionality wrt iff, implies functionality wrt iff, assert wf, eq id wf, assert-eq-id, poss-consistent wf, es-E wf, subtype rel wf, es-state wf, es-loc wf, trans wf, possible-event wf, event system wf, pe-state wf, es-state-when wf, es-state-after wf, Id wf, Id sq